Nuprl Lemma : divides_instance
2,24
postcript
pdf
3 | 6
latex
Definitions
t
T
,
Dec(
P
)
,
b
|
a
,
decidable
divides
,
x
:
A
.
B
(
x
)
,
outl(
x
)
,
P
Q
,
A
,
b
,
if
b
t
else
f
fi
,
isl(
x
)
,
iff
preserves
decidability
,
decidable
int
equal
,
true
,
True
Lemmas
not
wf
,
outl
wf
,
divides
wf
,
decidable
wf
,
decidable
divides
origin
T, Dec(P), b | a, decidable divides, 
x:A. B(x), outl(x), P 
Q, 
A, 
b, if b
t else f fi, isl(x), iff preserves decidability, decidable int equal, true
, True